Inference at * 2 1 1 
Iof proof for Lemma p-fun-exp-compose:

.....equality..... NILNIL

1. T : Type
2. n : 
3. 0 < n
4. h, f:(T(T + Top)). f^n - 1 o h   = primrec(n - 1;h;i,g. f o g  )
5. T(T + Top)
6. f : T(T + Top)
  primrec(1+(n - 1);p-id();i,g. f o g  ) = f o primrec(n - 1;p-id();i,g. f o g  )   

latex

 by GenConcl p-id() = id THENA Auto 

latex

 1: 

 1: 7. id : T(T + Top)
 1: 8. p-id() = id
 1:   primrec(1+(n - 1);id;i,g. f o g  ) = f o primrec(n - 1;id;i,g. f o g  )  
 .

Definitions	s = t, x:AB(x), left + right, Top, p-id(), P  Q, t  T, x:A. B(x)
Lemmas	p-id wf